\begin{tabbing}
update{-}spec(${\it ds}$;${\it da}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=${\it kz}$:Knd$\times$Id fp$\rightarrow$\+
\\[0ex]($\mathbb{N}\times$(State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;1of(${\it kz}$))$\rightarrow$fpf{-}cap(${\it ds}$;IdDeq;2of(${\it kz}$);Void))) List
\-
\end{tabbing}